/* Benchmarks for the PointerC verifier. */

// list visit

struct list 
{
  int data;
  struct list* next;
};

/*@ 
  @*/
struct list* createList(int n)
{
  struct list* l;
  struct list* p;
  int i;
  
  p = null;
  l = null;

  
  if (n>0){
    p = alloc (struct list);
    p->next = l;
    l = p;
    i = 1;
    while(i<=n-1) /*@({p, l}) && list(l->next) */ 
    {
      p = alloc(struct list);
      p->next = l;
      l = p;
      i = i + 1;
    }
    return l;
  }
  else
   return l;
}
/*@ */
  
